| Definitions | t  T,  x:A. B(x), ES(the_w), (Msg on l), type List, [], x:A  B(x), P & Q, A c B, {T}, P   Q, sender(e), let x,y = A in B(x;y), t.1, E,  b, sends(l,tg,e), s = t,  , Type, x:A  B(x), False,  A, Void,  x:A.B(x), Top, S  T, null(as), left + right,  , P  Q, P Q, IdLnk, Atom$n, Id, Dsys, D1 D2, World, FairFifo, PossibleWorld(D;w), rcv(l,tg), kind(e), Knd, (x l), @i: only L sends on (l with tg), D realizes es. P(es), only events in L send on l with tg, source(l), Msg, val(e), tag(e), lnk(e), msg(l;t;v), sends(l;e), {x:A| B(x)} , Msg(M), mtag(m), a = b,  x.A(x), <a, b>, SQType(T), s ~ t, lnk(k),  , #$n, ||as||, A  B,  , l[i], a < b, i  j , {i..j }, i j < k, True,  T,  x:A. B(x), index(e), tag(k), haslink(l;m), [car / cdr], outl(x), t.2, mtag(m) |